r,s:rationals. qle(r; s)  prop{i:l} 

latex

Definitions	t.1, grp_car(g), qadd_grp, qle(r; s), t  T, x:A. B(x), mon{i:l}, abmonoid{i:l}, ocmon{i:l}, ocgrp{i:l}
Lemmas	rationals wf, ocgrp wf, qadd grp wf2, grp leq wf